Search for: All records

Memory safety is an important property for security-critical systems, but it cannot be easily extended to cryptography, which is a common source of memory safety vulnerabilities. Cryptography libraries use assembly for direct control of timing and performance, but assembly introduces unsafety when it is called from a high-level memory-safe language like Rust. To enable quick and safe integration of assembly into Rust, specifically for building memory-safe cryptography, we present CLAMS. CLAMS verifies cryptographic assembly against safety constraints derived directly from Rust’s type system. Verification is done through symbolic execution at compile time to minimize run-time overheads, and supports verifying loops over potentially unbounded input buffers. CLAMS’s procedural macro interface forces developers to map safe Rust types to registers and define preconditions on input and output parameters. CLAMS’s techniques can verify the memory safety of assembly from a popular open-source cryptography library. We evaluated CLAMS and found that verification is quick and imposes compile-time overheads under 100ms and negligible run-time overheads. 

Tock began 10 years ago as a research operating system developed by academics to help other academics build urban sensing applications. By leveraging a new language (Rust) and new hardware protection mechanisms, Tock enabled “Multiprogramming a 64 kB Computer Safely and Effi­ciently”. Today, it is an open-source project with a vibrant community of users and contributors. It is deployed on root-of-trust hardware in data-center servers and on millions of laptops; it is used to develop automotive and space products, wearable electronics, and hardware security tokens—all while remaining a platform for operating systems research. This paper focuses on the impact of Tock’s technical design on its adoption, the challenges and unexpected benefits of using a type-safe language (Rust)—particularly in secu­rity-sensitive settings—and the experience of supporting a production open-source operating system from academia. 

Memory- and type-safe languages promise to eliminate entire classes of systems vulnerabilities by construction. In practice, though, even clean-slate systems often need to incor- porate libraries written in other languages with fewer safety guarantees. Because these interactions threaten the soundness of safe languages, they can reintroduce the exact vulnerabili- ties that safe languages prevent in the first place. This paper presents Omniglot: the first framework to effi- ciently uphold safety and soundness of Rust in the presence of unmodified and untrusted foreign libraries. Omniglot fa- cilitates interactions with foreign code by integrating with a memory isolation primitive and validation infrastructure, and avoids expensive operations such as copying or serialization. We implement Omniglot for two systems: we use it to inte- grate kernel components in a highly-constrained embedded operating system kernel, as well as to interface with conven- tional Linux userspace libraries. Omniglot performs com- parably to approaches that deliver weaker guarantees and significantly better than those with similar safety guarantees. 

Strictly serializable (linearizable) services appear to execute transactions (operations) sequentially, in an order consistent with real time. This restricts a transaction's (operation's) possible return values and in turn, simplifies application programming. In exchange, strictly serializable (linearizable) services perform worse than those with weaker consistency. But switching to such services can break applications. This work introduces two new consistency models to ease this trade-off: regular sequential serializability (RSS) and regular sequential consistency (RSC). They are just as strong for applications: we prove any application invariant that holds when using a strictly serializable (linearizable) service also holds when using an RSS (RSC) service. Yet they relax the constraints on services---they allow new, better-performing designs. To demonstrate this, we design, implement, and evaluate variants of two systems, Spanner and Gryff, relaxing their consistency to RSS and RSC, respectively. The new variants achieve better read-only transaction and read tail latency than their counterparts. 

Type-safe languages improve application safety by eliminating whole classes of vulnerabilities–such as buffer overflows–by construction. However, this safety sometimes comes with a performance cost. As a result, many modern type-safe languages provide escape hatches that allow developers to manually bypass them. The relative value of performance to safety and the degree of performance obtained depends upon the application context, including user goals and the hardware upon which the application is to be executed. Since libraries may be used in many different contexts, library developers cannot make safety-performance trade-off decisions appropriate for all cases. Application developers can tune libraries themselves to increase safety or performance, but this requires extra effort and makes libraries less reusable. To address this problem, we present NADER, a Rust development tool that makes applications safer by automatically transforming unsafe code into equivalent safe code according to developer preferences and application context. In end-to-end system evaluations in a given context, NADER automatically reintroduces numerous library bounds checks, in many cases making application code that uses popular Rust libraries safer with no corresponding loss in performance.